da:k:Knd fp Type, i:Id. da-outlinks(da;i)  (IdLnkIdType) List 

latex

Definitions	P  Q, P  Q, A & B, isrcv(k), lexpr{i}, Knd, b, x  dom(f), KindDeq, da-outlinks(da;i), mapfilter(f;P;L), has-src(i;k), IdLnk, Id, da-outlink-f(da;k), P & Q, fpf-dom-list(f), a:A fp B(a), Top, x. t(x), x:A. B(x), t  T
Lemmas	Knd wf, fpf-trivial-subtype-top, Kind-deq wf, fpf-dom-list wf, assert wf, fpf-dom wf, da-outlink-f wf, Id wf, IdLnk wf, has-src wf, mapfilter wf, fpf wf, isrcv wf, assert-has-src